-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}


import "LangPrelude.prg"

import "Thrist.omg"
  (Thrist, Nil, Cons, syntax List(l))


data Pair :: *1 ~> *1 ~> *1 where
  P :: forall (a :: *1) (b :: *1) . a ~> b ~> Pair a b
 deriving Pair(p)

kind Gate = GateClosed | GateOpen
kind Secondary = SecondaryEnabled | SecondaryBlocked
kind HandshakeIn = Idle | Requested
kind HandshakeOut = Idle' | NeedAck
kind Handshake = H HandshakeIn HandshakeOut

data State :: Gate ~> Secondary ~> Handshake ~> * where
  State :: [Transition g s h] -> State g s h


data Transition :: Gate ~> Secondary ~> Handshake ~> * where
  From :: State g' s' h'
       -> Obligation (g', s', h')p (g'', s'', h'')p
       -> Thrist Action (g'', s'', h'')p (g, s, h)p
       -> Transition g s h

data Obligation :: Pair Gate (Pair Secondary Handshake) ~> Pair Gate (Pair Secondary Handshake) ~> * where
  ExclusiveRequested :: Obligation (a, b, H Idle c)p (a, b, H Requested c)p
  AckReceived :: Obligation (a, b, H c NeedAck)p (a, b, H c Idle')p
  Plugged :: Obligation (GateClosed, b, H Idle c)p (GateClosed, b, H Idle c)p

data Action :: Pair Gate (Pair Secondary Handshake) ~> Pair Gate (Pair Secondary Handshake) ~> * where
  RequestExclusive :: Action (a, b, H c Idle')p (a, b, H c NeedAck)p
  AckExclusive :: Action (a, b, H Requested c)p (a, b, H Idle c)p
  OpenGate :: Action (GateClosed, SecondaryBlocked, c)p (GateOpen, SecondaryBlocked, c)p
  BlockSecondary :: Action (a, SecondaryEnabled, c)p (a, SecondaryBlocked, c)p
  -- ...

northWest :: State GateClosed SecondaryEnabled (H Idle Idle')
northWest = State []

north :: State GateClosed SecondaryEnabled (H Idle Idle')
north = State [From northWest ExclusiveRequested [AckExclusive]l]

west :: State GateClosed SecondaryEnabled (H Idle NeedAck)
west = State [From northWest Plugged [RequestExclusive]l]

mid :: State GateClosed SecondaryBlocked (H Idle NeedAck)
mid = State [ From west ExclusiveRequested [AckExclusive, BlockSecondary]l
	    , From north Plugged [RequestExclusive, BlockSecondary]l]

south :: State GateClosed SecondaryBlocked (H Idle Idle')
south = State [From west AckReceived [BlockSecondary]l]

southEast :: State GateOpen SecondaryBlocked (H Idle Idle')
southEast = State [ From mid AckReceived [OpenGate]l
		  , From south ExclusiveRequested [AckExclusive, OpenGate]l]
